D:dsys{i:l}. d-feasible{i:l}(D)  Prop{i'} 

latex

Definitions	t  T, x:A. B(x), P & Q, Prop, Feasible(D)
Lemmas	ma-feasible wf, subtype rel wf, ma-dout wf, ma-din wf, finite-type wf, IdLnk wf, Id wf, ldst wf, assert wf, ma-sends-on wf, d-m wf, lsrc wf, dsys wf